es:event_system{i:l}, e:es-E(es).
(es-isrcv(es; e))  (loc(es-sender(es; e)) = source(es-lnk(es; e))  Id) 

latex

Definitions	x:A. B(x), P  Q, t  T, guard(T), P  Q, prop{i:l}
Lemmas	es-loc-rcv, es-lnk wf, es-tag wf, assert wf, es-isrcv wf, es-E wf, event system wf